| contributor | FMI, Theoretische Informatik | ||||||||||||||||
| creator |
Göller, Stefan
| Lohrey, Markus
| date |
2006-02-08
| description |
47 pages
|
Model-checking problems for propositional dynamic logic (PDL) and
its extension PDL$^\cap$ (which includes the intersection operator
on programs) over various classes of infinite state systems (BPP,
BPA, pushdown systems, prefix-recognizable systems) are studied.
Precise upper and lower bounds are shown for the
data/expression/combined complexity of these model-checking
problems.
| format |
application/pdf
| 420573 Bytes | |
| identifier | http://www.informatik.uni-stuttgart.de/cgi-bin/NCSTRL/NCSTRL_view.pl?id=TR-2006-04&engl=1 |
| language | eng |
| publisher | Stuttgart, Germany, Universität Stuttgart |
| relation | Technical Report No. 2006/04 |
| source | ftp://ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart_fi/TR-2006-04/TR-2006-04.pdf |
| subject | Complexity Measures and Classes (CR F.1.3) |
| Mathematical Logic (CR F.4.1) | |
| infinite state systems | |
| model checking | |
| propositional dynamic logic | |
| basic parallel processes | |
| basic process algebras | |
| pushdown systems | |
| prefix-recognizable sytems | |
| title | Infinite State Model-Checking of Propositional Dynamic Logics |
| type | Text |
| Technical Report |